/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=NGR25/FONT#6=NGR20/FONT#7=MATH30/FONT#9=GRK30/FONT#10=MS25/FONT#11=GRFX25/FONT#12=GRFX35



␈↓ ↓H␈↓[This␈αis␈αa␈αreprint␈αwith␈αminor␈αchanges␈αof␈α"Correctness␈αof␈αa␈αCompiler␈αfor␈αArithmetic␈αExpressions"
␈↓ ↓H␈↓by␈α∞John␈α∞McCarthy␈α∞and␈α∞James␈α∞Painter␈α∞which␈α∞was␈α∞published␈α∞in␈α∞␈↓↓MATHEMATICAL␈α
ASPECTS
␈↓ ↓H␈↓↓OF␈α∩COMPUTER␈α∩SCIENCE␈↓␈α∩which␈α∩was␈α∪Volume␈α∩19␈α∩of␈α∩␈↓↓Proceedings␈α∩of␈α∩Symposia␈α∪in␈α∩Applied
␈↓ ↓H␈↓↓Mathematics␈↓ and published by the American Mathematical Society in 1967].

␈↓ ↓H␈↓α␈↓ β[Correctness of a Compiler for Arithmetic Expressions
␈↓ ↓H␈↓␈↓ ε8by
␈↓ ↓H␈↓␈↓ ∧cJohn McCarthy and James Painter



␈↓ ↓H␈↓1.  ␈↓αIntroduction.  ␈↓


␈↓ ↓H␈↓This␈α∂paper␈α∂contains␈α⊂a␈α∂proof␈α∂of␈α⊂the␈α∂correctness␈α∂of␈α∂a␈α⊂simple␈α∂compiling␈α∂algorithm␈α⊂for␈α∂compiling
␈↓ ↓H␈↓arithmetic expressions into machine language.

␈↓ ↓H␈↓The␈α∞definition␈α∞of␈α
correctness,␈α∞the␈α∞formalism␈α
used␈α∞to␈α∞express␈α
the␈α∞description␈α∞of␈α∞source␈α
language,
␈↓ ↓H␈↓object␈α
language␈α
and␈α
compiler,␈α
and␈α
the␈α
methods␈αof␈α
proof␈α
are␈α
all␈α
intended␈α
to␈α
serve␈α
as␈αprototypes␈α
for
␈↓ ↓H␈↓the␈α∞more␈α∞complicted␈α∞task␈α∞of␈α∞proving␈α∞the␈α∞correctness␈α∞of␈α∞usable␈α∞compilers.␈α∞ The␈α∞ultimate␈α∂goal,␈α∞as
␈↓ ↓H␈↓outlined␈αin␈αreferences␈α[1],␈α[2],␈α[3]␈αand␈α[4]␈αis␈αto␈αmake␈αit␈αpossible␈αto␈αuse␈αa␈αcomputer␈αto␈αcheck␈αproofs
␈↓ ↓H␈↓that compilers are correct.

␈↓ ↓H␈↓The␈αconcepts␈αof␈αabstract␈αsyntax,␈αstate␈αvector,␈α
the␈αuse␈αof␈αan␈αinterpreter␈αfor␈αdefining␈α
the␈αsemantics
␈↓ ↓H␈↓of␈αa␈αprogramming␈αlanguage,␈αand␈αthe␈αdefinition␈αof␈αcorrectness␈αof␈αa␈αcompiler␈αare␈αall␈αthe␈αsame␈αas␈αin
␈↓ ↓H␈↓[3].  The present paper, however, is the first in which the correctness of a compiler is proved.

␈↓ ↓H␈↓The␈α∂expressions␈α∂dealt␈α⊂with␈α∂in␈α∂this␈α⊂paper␈α∂are␈α∂formed␈α∂from␈α⊂constants␈α∂and␈α∂variables.␈α⊂ The␈α∂only
␈↓ ↓H␈↓operation␈αallowed␈αis␈αa␈αbinary␈α+␈αalthough␈αno␈αchange␈αin␈αmethod␈αwould␈αbe␈αrequired␈αto␈αinclude␈αany
␈↓ ↓H␈↓other binary operations.  An example of an expression that can be compiled is

␈↓ ↓H␈↓␈↓ αH␈↓↓(x + 3) + (x + (y + 2))␈↓

␈↓ ↓H␈↓although, because we use abstract syntax, no commitment to a particular notation is made.

␈↓ ↓H␈↓The␈α∞computer␈α
language␈α∞into␈α
which␈α∞these␈α
expressions␈α∞are␈α
compiled␈α∞is␈α
a␈α∞single␈α∞address␈α
computer
␈↓ ↓H␈↓with␈α∞an␈α∞accumulator,␈α∞called␈α∞␈↓↓ac,␈↓␈α∞and␈α∞four␈α∞instructions:␈α∞␈↓↓li␈↓␈α∞(load␈α∞immediate),␈α∞␈↓↓load,␈↓␈α∞␈↓↓sto␈↓␈α∞(store)␈α
and
␈↓ ↓H␈↓␈↓↓add.␈↓␈α Note␈αthat␈αthere␈αare␈αno␈αjump␈αinstructions.␈α Needless␈αto␈αsay,␈αthis␈αis␈αa␈αsevere␈αrestriction␈αon␈αthe
␈↓ ↓H␈↓generality of our results which we shall overcome in future work.

␈↓ ↓H␈↓The␈αcompiler␈αproduces␈αcode␈αthat␈αcomputes␈αthe␈αvalue␈αof␈αthe␈αexpression␈αbeing␈αcompiled␈αand␈α
leaves
␈↓ ↓H␈↓this␈α∞value␈α∞in␈α∂the␈α∞accumulator.␈α∞ The␈α∂above␈α∞expression␈α∞is␈α∞compiled␈α∂into␈α∞code␈α∞which␈α∂in␈α∞assembly
␈↓ ↓H␈↓language might look as follows:

␈↓ ↓H␈↓↓␈↓ αHload␈↓ β_x
␈↓ ↓H␈↓↓␈↓ αHsto␈↓ β_t
␈↓ ↓H␈↓↓␈↓ αHli␈↓ β_3
␈↓ ↓H␈↓↓␈↓ αHadd␈↓ β_t
␈↓ ↓H␈↓␈↓ εH␈↓ 92


␈↓ ↓H␈↓↓␈↓ αHsto␈↓ β_t
␈↓ ↓H␈↓↓␈↓ αHload␈↓ β_x
␈↓ ↓H␈↓↓␈↓ αHsto␈↓ β_t + 1
␈↓ ↓H␈↓↓␈↓ αHload␈↓ β_y
␈↓ ↓H␈↓↓␈↓ αHsto␈↓ β_t + 2
␈↓ ↓H␈↓↓␈↓ αHli␈↓ β_2
␈↓ ↓H␈↓↓␈↓ αHadd␈↓ β_t + 2
␈↓ ↓H␈↓↓␈↓ αHadd␈↓ β_t + 1
␈↓ ↓H␈↓↓␈↓ αHadd␈↓ β_t

␈↓ ↓H␈↓Again␈α∂because␈α∂we␈α∂are␈α∂using␈α∞abstract␈α∂syntax␈α∂there␈α∂is␈α∂no␈α∞commitment␈α∂to␈α∂a␈α∂precise␈α∂form␈α∂for␈α∞the
␈↓ ↓H␈↓object code.



␈↓ ↓H␈↓2.  ␈↓αThe source language. ␈↓


␈↓ ↓H␈↓The abstract analytic syntax of the source expressions is given by the table:

␈↓ ↓H␈↓␈↓ αH␈↓αpredicate␈↓ ∧xassociated functions

␈↓ ↓H␈↓↓␈↓ αHisconst(e)
␈↓ ↓H␈↓↓␈↓ αHisvar(e)
␈↓ ↓H␈↓↓␈↓ αHissum(e)␈↓ ∧xs1(e)     s2(e)

␈↓ ↓H␈↓which␈α∀asserts␈α∀that␈α∀the␈α∀expressions␈α∀comprise␈α∪constants,␈α∀variables␈α∀and␈α∀binary␈α∀sums,␈α∀that␈α∪the
␈↓ ↓H␈↓predicates␈α
␈↓↓isconst,␈α
isvar,␈α
␈↓and␈α
␈↓↓issum␈α
␈↓enable␈α
one␈α
to␈α
classify␈α
each␈α
expression␈α
and␈α
that␈α
each␈α
sum␈α␈↓↓e␈↓
␈↓ ↓H␈↓has summands ␈↓↓s1(e)␈↓ and ␈↓↓s2(e).␈↓

␈↓ ↓H␈↓The semantics is given by the formula

␈↓ ↓H␈↓␈↓ α8␈↓↓value(e,␈↓	x␈↓↓) ← ␈↓αif␈↓↓ isconst(e) ␈↓αthen␈↓↓ val(e) ␈↓αelse␈↓↓ ␈↓αif␈↓↓ isvar(e) ␈↓αthen␈↓↓ c(e,␈↓	x␈↓↓)␈↓
␈↓ ↓H␈↓(2.1)
␈↓ ↓H␈↓␈↓ α8␈↓↓␈↓αelse␈↓↓ ␈↓αif␈↓↓ issum(e) ␈↓αthen␈↓↓ value(s1(e),␈↓	x␈↓↓) + value(s2(e),␈↓	x␈↓↓)␈↓

␈↓ ↓H␈↓where␈α␈↓↓val(e)␈↓␈αgives␈αthe␈αnumerical␈αvalue␈αof␈αan␈αexpression␈α␈↓↓e␈↓␈αrepresenting␈αa␈αconstant,␈α␈↓↓c(e,␈↓	x␈↓↓)␈↓	␈α␈↓gives␈αthe
␈↓ ↓H␈↓value␈α∞of␈α∂the␈α∞variable␈α∂␈↓↓e␈↓␈α∞in␈α∞the␈α∂state␈α∞vector␈α∂␈↓	x␈↓␈α∞and␈α∂+␈α∞is␈α∞some␈α∂binary␈α∞operation.␈α∂ (It␈α∞is␈α∂natural␈α∞to
␈↓ ↓H␈↓regard␈α+␈αas␈αan␈αoperation␈αthat␈αresembles␈αaddition␈αof␈αreal␈αnumbers,␈αbut␈αour␈αresults␈αdo␈αnot␈αdepend
␈↓ ↓H␈↓on this).

␈↓ ↓H␈↓For␈α∞proving␈α∂the␈α∞correctness␈α∂of␈α∞compilers,␈α∂we␈α∞don't␈α∞need␈α∂a␈α∞synthetic␈α∂syntax␈α∞for␈α∂source␈α∞language
␈↓ ↓H␈↓expressions␈α∞since␈α∂the␈α∞interpreter␈α∂and␈α∞compiler␈α∂use␈α∞only␈α∂the␈α∞analytic␈α∂syntax.␈α∞ However,␈α∂we␈α∞shall
␈↓ ↓H␈↓need the following induction principle for expressions:

␈↓ ↓H␈↓Suppose␈α∞␈↓	F␈↓␈α∞is␈α∞a␈α∂predicate␈α∞applicable␈α∞to␈α∞expressions,␈α∞and␈α∂suppose␈α∞that␈α∞for␈α∞all␈α∞expressions␈α∂␈↓↓e,␈↓␈α∞we
␈↓ ↓H␈↓have
␈↓ ↓H␈↓␈↓ εH␈↓ 93


␈↓ ↓H␈↓↓␈↓ αHisconst(e) ⊃ ␈↓	F␈↓↓(e)  ␈↓and␈↓↓
␈↓ ↓H␈↓↓␈↓ αHisvar(e) ⊃ ␈↓	F␈↓↓(e)  ␈↓and␈↓↓
␈↓ ↓H␈↓↓␈↓ αHissum(e) ∧ ␈↓	F␈↓↓(s1(e)) ∧ ␈↓	F␈↓↓(s2(e)) ⊃ ␈↓	F␈↓↓(e).

␈↓ ↓H␈↓Then we may conclude that ␈↓	F␈↓␈↓↓(e) ␈↓is true for all expressions ␈↓↓e.␈↓



␈↓ ↓H␈↓3.  ␈↓αThe object language.␈↓


␈↓ ↓H␈↓We␈α∩must␈α⊃give␈α∩both␈α∩the␈α⊃analytic␈α∩and␈α∩synthetic␈α⊃syntaxes␈α∩for␈α∩the␈α⊃object␈α∩language␈α∩because␈α⊃the
␈↓ ↓H␈↓interpreter␈α⊂defining␈α⊂its␈α⊂semantics␈α⊂uses␈α⊂the␈α⊂analytic␈α⊂syntax␈α⊂and␈α⊂the␈α⊂compiler␈α⊂uses␈α⊃the␈α⊂synthetic
␈↓ ↓H␈↓syntax.  We may write the analytic and synthetic syntaxes for instructions in the following table.

␈↓ ↓H␈↓␈↓ α8␈↓αoperation␈↓ βxpredicate␈↓ ¬8analytic operation␈↓ πXsynthetic operation

␈↓ ↓H␈↓↓␈↓ αHli␈↓ β_␈↓	a␈↓↓␈↓ βxisli(s)␈↓ ¬xarg(s)␈↓ λ_mkli(␈↓	a␈↓↓)
␈↓ ↓H␈↓↓␈↓ αHload␈↓ β_x␈↓ βxisload(s)␈↓ ¬xadr(s)␈↓ λ_mkload(x)
␈↓ ↓H␈↓↓␈↓ αHsto␈↓ β_x␈↓ βxissto(s)␈↓ ¬xadr(s)␈↓ λ_mksto(x)
␈↓ ↓H␈↓↓␈↓ αHadd␈↓ β_x␈↓ βxisadd(s)␈↓ ¬xadr(s)␈↓ λ_mkadd(x)

␈↓ ↓H␈↓A␈αprogram␈αis␈αa␈αlist␈αof␈αinstructions␈αand␈α␈↓↓null(p)␈↓␈αasserts␈αthat␈α␈↓↓p␈↓␈αis␈αthe␈αnull␈αlist.␈α If␈αthe␈αprogram␈α␈↓↓p␈↓␈αis
␈↓ ↓H␈↓not␈αnull␈αthen␈α␈↓↓first(p)␈↓␈αgives␈αthe␈αfirst␈α
instruction␈αand␈α␈↓↓rest(p)␈↓␈αgives␈αthe␈αlist␈αof␈αremaining␈α
instructions.
␈↓ ↓H␈↓We␈αshall␈αuse␈αthe␈αoperation␈α␈↓↓p1*p2␈↓␈αto␈αdenote␈αthe␈αprogram␈αobtained␈αby␈αappending␈α␈↓↓p2␈↓␈αonto␈αthe␈αend
␈↓ ↓H␈↓of␈α
␈↓↓p1.␈↓␈α
 Since␈αwe␈α
have␈α
only␈αone␈α
level␈α
of␈αlist␈α
we␈α
can␈αidentify␈α
a␈α
single␈αinstruction␈α
with␈α
a␈αprogram
␈↓ ↓H␈↓that has just one instruction.

␈↓ ↓H␈↓The synthetic and analytic syntaxes of instructions are related by the following.

␈↓ ↓H␈↓↓␈↓ αXisli(mkli(␈↓	a␈↓↓))
␈↓ ↓H␈↓↓␈↓ αX␈↓	a␈↓↓ = arg(mkli(␈↓	a␈↓↓))
␈↓ ↓H␈↓↓(3.1)␈↓ αXisli(s) ⊃ s = mkli(arg(s))
␈↓ ↓H␈↓↓␈↓ αXnull(rest(mkli(␈↓	a␈↓↓)))
␈↓ ↓H␈↓↓␈↓ αXisli(s) ⊃ first(s) = s

␈↓ ↓H␈↓↓␈↓ αXisload(mkload(x))
␈↓ ↓H␈↓↓␈↓ αXx = adr(mkload(x))
␈↓ ↓H␈↓↓(3.2)␈↓ αXisload(x) ⊃ x = mkload(adr(x))
␈↓ ↓H␈↓↓␈↓ αXnull(rest(mkload(x)))
␈↓ ↓H␈↓↓␈↓ αXisload(s) ⊃ first(s) = s

␈↓ ↓H␈↓↓␈↓ αXissto(mksto(x))
␈↓ ↓H␈↓↓␈↓ αXx = adr(mksto(x))
␈↓ ↓H␈↓↓(3.3)␈↓ αXissto(x) ⊃ x = mksto(adr(x))
␈↓ ↓H␈↓↓␈↓ αXnull(rest(mksto(x)))
␈↓ ↓H␈↓↓␈↓ αXissto(s) ⊃ first(s) = s
␈↓ ↓H␈↓␈↓ εH␈↓ 94


␈↓ ↓H␈↓↓␈↓ αXisadd(mkadd(x))
␈↓ ↓H␈↓↓␈↓ αXx = adr(mkadd(x))
␈↓ ↓H␈↓↓(3.4)␈↓ αXisadd(x) ⊃ x = mkadd(adr(x))
␈↓ ↓H␈↓↓␈↓ αXnull(rest(mkadd(x)))
␈↓ ↓H␈↓↓␈↓ αXisadd(x) ⊃ first(s) = s

␈↓ ↓H␈↓↓(3.5)␈↓ αX¬null(p) ⊃ p = first(p) * rest(p),

␈↓ ↓H␈↓↓(3.6)     ¬null(p1) ∧ null(rest(p1)) ⊃ p1 = first(p1*p2)

␈↓ ↓H␈↓↓(3.7)␈↓ αXnull(p1*p2) ≡ null(p1) ∧ null(p2).

␈↓ ↓H␈↓The␈α⊃*␈α⊃operation␈α⊃is␈α⊃associative.␈α⊃(The␈α⊃somewhat␈α⊃awkward␈α⊃form␈α⊃of␈α⊃these␈α⊃relations␈α⊃comes␈α⊃from
␈↓ ↓H␈↓having␈α⊂a␈α∂general␈α⊂concatenation␈α∂operation␈α⊂rather␈α∂than␈α⊂just␈α∂an␈α⊂operation␈α∂that␈α⊂prefixes␈α⊂a␈α∂single
␈↓ ↓H␈↓instruction onto a program.)

␈↓ ↓H␈↓A␈αstate␈αvector␈αfor␈αa␈αmachine␈αgives,␈αfor␈αeach␈αregister␈αin␈αthe␈αmachine,␈αits␈αcontents.␈α We␈αinclude␈αthe
␈↓ ↓H␈↓accumulator␈αdenoted␈αby␈α
␈↓↓ac␈↓␈αas␈αa␈α
register.␈α There␈αare␈α
two␈αfunctions␈αof␈α
state␈αvectors␈αas␈αintroduced␈α
in
␈↓ ↓H␈↓[3], namely

␈↓ ↓H␈↓1.  ␈↓↓c(x,␈↓	h␈↓↓) ␈↓denotes the value of the contents of register ␈↓↓x␈↓ in machine state ␈↓	h␈↓.

␈↓ ↓H␈↓2.␈α∂ ␈↓↓a(x,␈↓	a␈↓↓,␈↓	h␈↓↓)␈α∂␈↓denotes␈α∂the␈α∂state␈α∂vector␈α∂that␈α∂is␈α∂obtained␈α∂from␈α∂the␈α∂state␈α∂vector␈α∂␈↓	h␈↓␈α∂by␈α∂changing␈α∞the
␈↓ ↓H␈↓contents of register ␈↓↓x␈↓ to ␈↓	a␈↓ leaving the other registers unaffected.

␈↓ ↓H␈↓These functions satisfy the following relations:


␈↓ ↓H␈↓(3.8)␈↓ ∧,␈↓↓c(x,a(y,␈↓	a␈↓↓,␈↓	h␈↓↓)) = ␈↓αif␈↓↓ x = y ␈↓αthen␈↓↓ ␈↓	a␈↓↓ ␈↓αelse␈↓↓ c(x,␈↓	h␈↓↓),␈↓ 

␈↓ ↓H␈↓(3.9)␈↓ β#␈↓↓a(x,␈↓	a␈↓↓,a(y,␈↓	b␈↓↓,␈↓	h␈↓↓)) = ␈↓αif␈↓↓ x = y ␈↓αthen␈↓↓ a(x,␈↓	a␈↓↓,␈↓	h␈↓↓) ␈↓αelse␈↓↓ a(y,␈↓	b␈↓↓,a(x,␈↓	a␈↓↓,␈↓	h␈↓↓)),␈↓ 

␈↓ ↓H␈↓(3.10)␈↓ ¬Q␈↓↓a(x,c(x,␈↓	h␈↓↓),␈↓	h␈↓↓) = ␈↓	h␈↓↓.␈↓ 

␈↓ ↓H␈↓Now we can define the semantics of the object language by

␈↓ ↓H␈↓↓␈↓ αXstep(x,␈↓	h␈↓↓) ← ␈↓αif␈↓↓ isli(s) ␈↓αthen␈↓↓ a(ac,arg(s),␈↓	h␈↓↓) ␈↓αelse␈↓↓ ␈↓αif␈↓↓
␈↓ ↓H␈↓↓␈↓ αXisload(s) ␈↓αthen␈↓↓ a(ac,c(adr(s),␈↓	h␈↓↓),␈↓	h␈↓↓) ␈↓αelse␈↓↓ ␈↓αif␈↓↓
␈↓ ↓H␈↓↓(3.11)␈↓ αXissto(s) ␈↓αthen␈↓↓ a(adr(s),c(ac,␈↓	h␈↓↓),␈↓	h␈↓↓) ␈↓αelse␈↓↓ ␈↓αif␈↓↓
␈↓ ↓H␈↓↓␈↓ αXisadd(s) ␈↓αthen␈↓↓ a(ac,c(adr(s),␈↓	h␈↓↓) + c(ac,␈↓	h␈↓↓),␈↓	h␈↓↓)

␈↓ ↓H␈↓which gives the state vector that results from executing an instruction and

␈↓ ↓H␈↓(3.12)␈↓ β
␈↓↓outcome(p,␈↓	h␈↓↓) ← ␈↓αif␈↓↓ null(p) ␈↓αthen␈↓↓ ␈↓	h␈↓↓ ␈↓αelse␈↓↓ outcome(rest(p),step(first(p),␈↓	h␈↓↓))␈↓ 

␈↓ ↓H␈↓which gives the state vector that results from executing the program ␈↓↓p␈↓ with state vector ␈↓	h␈↓.

␈↓ ↓H␈↓The following lemma is left as and exercise for the reader.
␈↓ ↓H␈↓␈↓ εH␈↓ 95


␈↓ ↓H␈↓(3.13)␈↓ ∧_␈↓↓outcome(p1*p2,␈↓	h␈↓↓) = outcome(p2,outcome(p1,␈↓	h␈↓↓))␈↓ 



␈↓ ↓H␈↓4.  ␈↓αThe compiler.␈↓


␈↓ ↓H␈↓We␈αshall␈αassume␈αthat␈αthere␈αis␈αa␈αmap␈αgiving␈αfor␈αeach␈αvariable␈αin␈αthe␈αexpression␈αa␈αlocation␈αin␈αthe
␈↓ ↓H␈↓main memory of the machine.  ␈↓↓loc(v)␈↓ gives this location and we shall assume

␈↓ ↓H␈↓(4.1)␈↓ ¬R␈↓↓c(loc(v),␈↓	h␈↓↓) = c(v,␈↓	x␈↓↓)␈↓ 

␈↓ ↓H␈↓as␈α
a␈α∞relation␈α
between␈α∞the␈α
state␈α∞vector␈α
␈↓	h␈↓␈α∞before␈α
the␈α∞compiled␈α
program␈α∞starts␈α
to␈α∞act␈α
and␈α∞the␈α
state
␈↓ ↓H␈↓vector ␈↓	x␈↓ of the source program.

␈↓ ↓H␈↓Now we can write the compiler.  It is

␈↓ ↓H␈↓␈↓ ∧2␈↓↓compile(e,t) ← ␈↓αif␈↓↓ isconst(e) ␈↓αthen␈↓↓ mkli(val(e))␈↓ 

␈↓ ↓H␈↓(4.2)␈↓ ∧L␈↓↓␈↓αelse␈↓↓ ␈↓αif␈↓↓ isvar(e) ␈↓αthen␈↓↓ mkload(loc(e,map))␈↓ 

␈↓ ↓H␈↓␈↓ αA␈↓↓␈↓αelse␈↓↓ ␈↓αif␈↓↓ issum(e) ␈↓αthen␈↓↓ compile(s1(e),t) * mksto(t) * compile(s2(e),t + 1) * mkadd(t)␈↓ 

␈↓ ↓H␈↓Here␈α∞␈↓↓t␈↓␈α∞is␈α∞the␈α
number␈α∞of␈α∞a␈α∞register␈α
such␈α∞that␈α∞all␈α∞variables␈α
are␈α∞stored␈α∞in␈α∞registers␈α∞numbered␈α
less
␈↓ ↓H␈↓than ␈↓↓t,␈↓ so that registers ␈↓↓t␈↓ and above are available for temporary storage.

␈↓ ↓H␈↓Before␈α∂we␈α∂can␈α∂state␈α∂our␈α∂definition␈α∂of␈α⊂correctness␈α∂of␈α∂the␈α∂compiler,␈α∂we␈α∂need␈α∂a␈α∂notion␈α⊂of␈α∂partial
␈↓ ↓H␈↓equality for state vectors

␈↓ ↓H␈↓␈↓ ε∪␈↓↓␈↓	z␈↓↓␈↓β1␈↓↓ =␈↓βA␈↓↓ ␈↓	z␈↓↓␈↓β2␈↓↓␈↓ 

␈↓ ↓H␈↓where␈α∀␈↓	z␈↓␈↓β1␈↓␈α∀and␈α∀␈↓	z␈↓␈↓β2␈↓␈α∀are␈α∀state␈α∀vectors␈α∀and␈α∀␈↓↓A␈↓␈α∀is␈α∀a␈α∀set␈α∀of␈α∀variables␈α∀means␈α∀that␈α∪corresponding
␈↓ ↓H␈↓components␈αof␈α␈↓	z␈↓␈↓β1␈↓␈αand␈α␈↓	z␈↓␈↓β2␈↓␈αare␈αequal␈αexcept␈αpossibly␈αfor␈αvalues,␈αof␈αvariables␈αin␈α␈↓↓A.␈↓␈α Symbolically,␈α␈↓↓x
␈↓ ↓H␈↓↓␈↓ππ ␈↓↓A ⊃ c(x,␈↓	z␈↓↓␈↓β1␈↓↓) = c(x,␈↓	z␈↓↓␈↓β2␈↓↓)␈↓.  Partial equality satisfies the following relations:

␈↓ ↓H␈↓(4.3)␈↓ β ␈↓↓␈↓	z␈↓↓␈↓β1␈↓↓ = ␈↓	z␈↓↓␈↓β2␈↓↓ ␈↓is equivalent to ␈↓	z␈↓␈↓β1␈↓ =␈↓β{ }␈↓ ␈↓	z␈↓␈↓β2␈↓ where { } denotes the empty set, 

␈↓ ↓H␈↓(4.4)␈↓ ∧]␈↓↓␈↓if ␈↓↓A ⊂ B␈↓ and ␈↓	z␈↓␈↓β1␈↓ =␈↓βA␈↓ ␈↓	z␈↓␈↓β2␈↓ then ␈↓	z␈↓␈↓β1␈↓ =␈↓βB␈↓ ␈↓	z␈↓␈↓β2␈↓, 

␈↓ ↓H␈↓(4.5)␈↓ ∧'␈↓↓␈↓if ␈↓	z␈↓␈↓β1␈↓ =␈↓βA␈↓ ␈↓	z␈↓␈↓β2␈↓, then ␈↓↓a(x,␈↓	a␈↓↓,␈↓	z␈↓↓␈↓β1␈↓↓) =␈↓βA-{x} ␈↓↓a(x,␈↓	a␈↓↓,␈↓	z␈↓↓␈↓β2␈↓↓),␈↓ 

␈↓ ↓H␈↓(4.6)␈↓ ¬∂␈↓↓␈↓if ␈↓↓x ε A ␈↓then ␈↓↓a(x,␈↓	a␈↓↓,␈↓	z␈↓↓) =␈↓βA␈↓↓ ␈↓	z␈↓↓,␈↓ 

␈↓ ↓H␈↓(4.7)␈↓ ∧?␈↓↓␈↓if ␈↓	z␈↓␈↓β1␈↓ =␈↓βA␈↓ ␈↓	z␈↓␈↓β2␈↓ and ␈↓	z␈↓␈↓β2␈↓ =␈↓βB␈↓ ␈↓	z␈↓␈↓β3␈↓, then ␈↓	z␈↓␈↓β1␈↓ =␈↓βA∪B␈↓ ␈↓	z␈↓␈↓β3␈↓. 

␈↓ ↓H␈↓In our case we need a specialization of this notation and will use

␈↓ ↓H␈↓␈↓ α8␈↓↓␈↓	z␈↓↓␈↓β1␈↓↓ =␈↓βt␈↓ ␈↓	z␈↓␈↓β2␈↓ to denote ␈↓	z␈↓␈↓β1␈↓ =␈↓β{x|x≥t} ␈↓␈↓	z␈↓␈↓β2␈↓
␈↓ ↓H␈↓␈↓ εH␈↓ 96


␈↓ ↓H␈↓and
␈↓ ↓H␈↓␈↓ α8␈↓↓␈↓	z␈↓↓␈↓β1␈↓↓ =␈↓βac␈↓ ␈↓	z␈↓␈↓β2␈↓ to denote ␈↓	z␈↓␈↓β1␈↓ =␈↓β{ac} ␈↓␈↓	z␈↓␈↓β2␈↓
␈↓ ↓H␈↓and
␈↓ ↓H␈↓␈↓ α8␈↓↓␈↓	z␈↓↓␈↓β1␈↓↓ =␈↓βt,ac␈↓ ␈↓	z␈↓␈↓β2␈↓ to denote a␈↓	z␈↓␈↓β1␈↓ =␈↓β{x|x = ac ∨ x ≥ t} ␈↓␈↓	z␈↓␈↓β2␈↓. 

␈↓ ↓H␈↓The correctness of the compiler is stated in

␈↓ ↓H␈↓THEOREM 1.  ␈↓↓If ␈↓	h␈↓↓ and ␈↓	x␈↓↓ are machine and source language state vectors respectively such that

␈↓ ↓H␈↓↓(4.8) c(loc(v),␈↓	h␈↓↓) = c(v,␈↓	x␈↓↓), then
␈↓ ↓H␈↓↓␈↓ ∧Xoutcome(compile(e,t),␈↓	h␈↓↓) =␈↓βt␈↓↓ a(ac,value(e,␈↓	x␈↓↓),␈↓	h␈↓↓).

␈↓ ↓H␈↓↓␈↓It␈α∞states␈α∞that␈α∞the␈α∞result␈α∞of␈α∞running␈α∞the␈α∞compiled␈α∞program␈α∞is␈α∞to␈α∞put␈α∞the␈α∞value␈α∞of␈α∞the␈α∞expression
␈↓ ↓H␈↓compiled␈αinto␈αthe␈αaccumulator.␈α No␈αregisters␈αexcept␈αthe␈αaccumulator␈αand␈αthose␈αwith␈αaddresses␈α≥␈α␈↓↓t␈↓
␈↓ ↓H␈↓are affected.



␈↓ ↓H␈↓5.  ␈↓αProof of Theorem 1.␈↓


␈↓ ↓H␈↓The␈αproof␈αis␈α
accomplished␈αby␈αan␈α
induction␈αon␈αthe␈α
expression␈α␈↓↓e␈↓␈αbeing␈α
compiled.␈α We␈αprove␈αit␈α
first
␈↓ ↓H␈↓for␈αconstants,␈αthen␈αfor␈αvariables,␈αand␈αthen␈αfor␈αsums␈αon␈αthe␈αinduction␈αhypothesis␈αthat␈αit␈αis␈αtrue␈αfor
␈↓ ↓H␈↓the summands.  Thus there are three cases.

␈↓ ↓H␈↓I.  ␈↓↓isconst(e).  ␈↓We have␈↓ πX␈↓αJustification␈↓

␈↓ ↓H␈↓␈↓↓outcome(compile(e,t),␈↓	h␈↓↓)␈↓ ∧H= outcome(mkli(val(e)),␈↓	h␈↓↓)␈↓ λ(4.2
␈↓ ↓H␈↓↓␈↓ ∧H= step(mkli(val(e)),␈↓	h␈↓↓)␈↓ λ(3.12, 3.1
␈↓ ↓H␈↓↓␈↓ ∧H= a(ac,arg(mkli(val(e))),␈↓	h␈↓↓)␈↓ λ(3.1, 3.11
␈↓ ↓H␈↓↓␈↓ ∧H= a(ac,val(e),␈↓	h␈↓↓)␈↓ λ(3.1
␈↓ ↓H␈↓↓␈↓ ∧H= a(ac,value(e,␈↓	x␈↓↓),␈↓	h␈↓↓)␈↓ λ(2.1
␈↓ ↓H␈↓↓␈↓ ∧H=␈↓βt␈↓↓ a(ac,value(e,␈↓	x␈↓↓),␈↓	h␈↓↓).␈↓ λ(4.3, 4.4


␈↓ ↓H␈↓↓␈↓II.  ␈↓↓isvar(e).  ␈↓We have

␈↓ ↓H␈↓␈↓↓outcome(compile(e,t),␈↓	h␈↓↓)␈↓ ∧λ= outcome(mkload(loc(e)),␈↓	h␈↓↓)␈↓ λ(4.2
␈↓ ↓H␈↓↓␈↓ ∧λ= a(ac,c(adr(mkload(loc(e))),␈↓	h␈↓↓,␈↓	h␈↓↓)␈↓ λ(3.12, 3.2, 3.11
␈↓ ↓H␈↓↓␈↓ ∧λ= a(ac,c(loc(e),␈↓	h␈↓↓),␈↓	h␈↓↓)␈↓ λ(3.2
␈↓ ↓H␈↓↓␈↓ ∧λ= a(ac,c(e,␈↓	x␈↓↓),␈↓	h␈↓↓)␈↓ λ(4.1
␈↓ ↓H␈↓↓␈↓ ∧λ= a(ac,value(e,␈↓	x␈↓↓),␈↓	h␈↓↓)␈↓ λ(2.1
␈↓ ↓H␈↓↓␈↓ ∧λ=␈↓βt␈↓↓ a(ac,value(e,␈↓	x␈↓↓),␈↓	h␈↓↓).␈↓ λ(4.3, 4.4


␈↓ ↓H␈↓↓␈↓III.  ␈↓↓issum(e).  ␈↓In this case, we first write

␈↓ ↓H␈↓␈↓↓outcome(compile(e,t),␈↓	h␈↓↓)
␈↓ ↓H␈↓␈↓ εH␈↓ 97


␈↓ ↓H␈↓↓␈↓ ↓x= outcome(compile(s1(e),t) * mksto(t)
␈↓ ↓H␈↓↓␈↓ βx* compile(s2(e),t + 1) * mkadd(t),␈↓	h␈↓↓)␈↓ λ(4.2
␈↓ ↓H␈↓↓␈↓ ↓x= outcome(mkadd(t),outcome(compile(s2(e),t + 1),
␈↓ ↓H␈↓↓␈↓ αXoutcome(mksto(t),outcome(compile(s1(e),t),␈↓	h␈↓↓)))␈↓ λ(3.13

␈↓ ↓H␈↓using␈α∞the␈α∞relation␈α∞between␈α∞concatenating␈α∞programs␈α∞and␈α∞composing␈α∞the␈α∞functions␈α∂they␈α∞represent.
␈↓ ↓H␈↓Now we introduce some notation.  Let

␈↓ ↓H␈↓␈↓ βx␈↓↓v = value(e,␈↓	x␈↓↓),
␈↓ ↓H␈↓↓␈↓ βxv␈↓β1␈↓↓ = value(s1(e),␈↓	x␈↓↓),
␈↓ ↓H␈↓↓␈↓ βxv␈↓β2␈↓↓ = value(s2(e),␈↓	x␈↓↓),

␈↓ ↓H␈↓so that ␈↓↓v = v␈↓β1␈↓↓ + v␈↓β2␈↓↓␈↓.  Further let

␈↓ ↓H␈↓␈↓ β(␈↓↓␈↓	z␈↓↓␈↓β1␈↓↓ = outcome(compile(s1(e),t),␈↓	h␈↓↓),
␈↓ ↓H␈↓↓␈↓ β(␈↓	z␈↓↓␈↓β2␈↓↓ = outcome(mksto(t),␈↓	z␈↓↓␈↓β1␈↓↓),
␈↓ ↓H␈↓↓␈↓ β(␈↓	z␈↓↓␈↓β3␈↓↓ = outcome(compile(s2(e),t + 1),␈↓	z␈↓↓␈↓β2␈↓↓),
␈↓ ↓H␈↓↓␈↓ β(␈↓	z␈↓↓␈↓β4␈↓↓ = outcome(mkadd(t),␈↓	z␈↓↓␈↓β3␈↓↓)

␈↓ ↓H␈↓so that ␈↓↓␈↓	z␈↓↓␈↓β4␈↓↓ = outcome(compile(e,t),␈↓	h␈↓↓)␈↓, and the statement to be proved becomes

␈↓ ↓H␈↓␈↓ ¬`␈↓↓␈↓	z␈↓↓␈↓β4␈↓↓ =␈↓βt␈↓↓ a(ac,v,␈↓	h␈↓↓).␈↓ 

␈↓ ↓H␈↓We have

␈↓ ↓H␈↓␈↓↓␈↓ α8␈↓	z␈↓↓␈↓β1␈↓↓␈↓ αX= outcome(compile(s1(e),t),␈↓	h␈↓↓)
␈↓ ↓H␈↓↓␈↓ α8␈↓ αX=␈↓βt␈↓↓ a(ac,v␈↓β1␈↓↓,␈↓	h␈↓↓)  ␈↓ ε8␈↓Induction Hypothesis

␈↓ ↓H␈↓and

␈↓ ↓H␈↓␈↓ α8␈↓↓c(ac,␈↓	z␈↓↓␈↓β1␈↓↓) = v␈↓β1␈↓↓.␈↓ ε83.8

␈↓ ↓H␈↓↓␈↓Now␈↓↓
␈↓ ↓H␈↓↓␈↓ α8␈↓	z␈↓↓␈↓β2␈↓↓␈↓ αX= outcome(mksto(t),␈↓	z␈↓↓␈↓β1␈↓↓)
␈↓ ↓H␈↓↓␈↓ α8␈↓ αX= a(t,c(ac,␈↓	z␈↓↓␈↓β1␈↓↓),␈↓	z␈↓↓␈↓β1␈↓↓)␈↓ ε83.12, 3.3, 3.11
␈↓ ↓H␈↓↓␈↓ α8␈↓ αX= a(t,v␈↓β1␈↓↓,␈↓	z␈↓↓␈↓β1␈↓↓)␈↓ ε8␈↓Substitution␈↓↓
␈↓ ↓H␈↓↓␈↓ α8␈↓ αX=␈↓βt+1␈↓↓ a(t,v␈↓β1␈↓↓,a(ac,v␈↓β1␈↓↓,␈↓	h␈↓↓))␈↓ ε84.5
␈↓ ↓H␈↓↓␈↓ α8␈↓ αX=␈↓βt+1,ac␈↓↓ a(t,v␈↓β1␈↓↓,␈↓	h␈↓↓)␈↓ ε84.6, 3.9
␈↓ ↓H␈↓↓␈↓and␈↓↓
␈↓ ↓H␈↓↓␈↓ α8c(t,␈↓	z␈↓↓␈↓β2␈↓↓) = v␈↓β1␈↓↓.␈↓ ε83.8
␈↓ ↓H␈↓↓␈↓Next␈↓↓
␈↓ ↓H␈↓↓␈↓ α8␈↓	z␈↓↓␈↓β3␈↓↓␈↓ αX= outcome(compile(s2(e),t + 1),␈↓	z␈↓↓␈↓β2␈↓↓)
␈↓ ↓H␈↓↓␈↓ α8␈↓ αX=␈↓βt+1␈↓↓ a(ac,v␈↓β2␈↓↓,␈↓	z␈↓↓␈↓β2␈↓↓).
␈↓ ↓H␈↓␈↓ εH␈↓ 98


␈↓ ↓H␈↓Here␈αwe␈αuse␈αthe␈α
induction␈αhypothesis␈αagain␈αto␈α
assume␈αthat␈α␈↓↓s2(e)␈↓␈αis␈α
compiled␈αcorrectly.␈α In␈αorder␈α
to
␈↓ ↓H␈↓apply it, we need ␈↓↓c(loc(v),␈↓	z␈↓↓␈↓β2␈↓↓) = c(v,␈↓	x␈↓↓) ␈↓ for each variable ␈↓↓v␈↓ which is proved as follows:

␈↓ ↓H␈↓␈↓ αH␈↓↓c(loc(v),␈↓	z␈↓↓␈↓β2␈↓↓)␈↓ ∧(= c(loc(v),a(t,v␈↓β1␈↓↓,␈↓	h␈↓↓)) ␈↓since ␈↓↓loc(v) < t
␈↓ ↓H␈↓↓␈↓ αH␈↓ ∧(␈↓ ∧8= c(loc(v),␈↓	h␈↓↓) ␈↓for the same reason␈↓↓
␈↓ ↓H␈↓↓␈↓ αH␈↓ ∧(␈↓ ∧8= c(v,␈↓	x␈↓↓) ␈↓by the hypothesis of the theorem.

␈↓ ↓H␈↓Now we can continue with

␈↓ ↓H␈↓␈↓↓␈↓ α8␈↓	z␈↓↓␈↓β3␈↓↓ = ␈↓βt+1␈↓↓ a(ac,v␈↓β2␈↓↓,a(t,v␈↓β1␈↓↓,␈↓	h␈↓↓))␈↓ ε83.9, 4.5
␈↓ ↓H␈↓↓␈↓and␈↓↓
␈↓ ↓H␈↓↓␈↓ α8c(ac,␈↓	z␈↓↓␈↓β3␈↓↓) = v␈↓β2␈↓↓ ␈↓and ␈↓↓c(t,␈↓	z␈↓↓␈↓β3␈↓↓) = v␈↓β1␈↓↓.␈↓ ε83.8
␈↓ ↓H␈↓↓␈↓Finally,␈↓↓
␈↓ ↓H␈↓↓␈↓ α8␈↓	z␈↓↓␈↓β4␈↓↓␈↓ αX= outcome(mkadd(t),␈↓	z␈↓↓␈↓β3␈↓↓)
␈↓ ↓H␈↓↓␈↓ α8␈↓ αX= a(ac,c(t,␈↓	z␈↓↓␈↓β3␈↓↓) + c(ac,␈↓	z␈↓↓␈↓β3␈↓↓),␈↓	z␈↓↓␈↓β3␈↓↓)␈↓ ε83.12, 3.4, 3.11
␈↓ ↓H␈↓↓␈↓ α8␈↓ αX= a(ac,v,␈↓	z␈↓↓␈↓β3␈↓↓)␈↓ ε8␈↓Definition of ␈↓↓v,␈↓ substitution␈↓↓
␈↓ ↓H␈↓↓␈↓ α8␈↓ αX=␈↓βt+1␈↓↓ a(ac,v,a(ac,v␈↓β2␈↓↓,a(t,v␈↓β1␈↓↓,␈↓	h␈↓↓)))␈↓ ε84.5
␈↓ ↓H␈↓↓␈↓ α8␈↓ αX=␈↓βt+1␈↓↓ a(ac,v,a(t,v␈↓β1␈↓↓,␈↓	h␈↓↓))␈↓ ε83.9
␈↓ ↓H␈↓↓␈↓ α8␈↓ αX=␈↓βt␈↓↓ a(ac,v,␈↓	h␈↓↓).␈↓ ε83.9, 4.6, 4.7

␈↓ ↓H␈↓This concludes the proof.



␈↓ ↓H␈↓6.  ␈↓αRemarks.␈↓


␈↓ ↓H␈↓The␈α∂problem␈α∂of␈α∂the␈α∂relations␈α∂between␈α∂source␈α∂language␈α∂and␈α∂object␈α∂language␈α∂arithmetic␈α∂is␈α∞dealt
␈↓ ↓H␈↓with␈αhere␈αby␈αassuming␈αthat␈αthe␈α+␈αsigns␈αin␈αformulas␈α(2.1)␈αand␈α(3.11)␈αwhich␈αdefine␈αthe␈αsemantics␈αof
␈↓ ↓H␈↓the␈α∞source␈α∞and␈α∞object␈α∞languages␈α∞represent␈α∞the␈α
same␈α∞operation.␈α∞ Theorem␈α∞1␈α∞does␈α∞not␈α∞depend␈α
on
␈↓ ↓H␈↓any properties of this operation, not even commutativity or associativity.

␈↓ ↓H␈↓The␈αproof␈αis␈αentirely␈αstraightforward␈αonce␈αthe␈αnecessary␈αmachinery␈αhas␈αbeen␈αcreated.␈α Additional
␈↓ ↓H␈↓operations␈α∩such␈α∩as␈α∪subtraction,␈α∩multiplication␈α∩and␈α∩division␈α∪could␈α∩be␈α∩added␈α∪without␈α∩essential
␈↓ ↓H␈↓change in the proof.

␈↓ ↓H␈↓For example, to put multiplication into the system the following changes would be required.

␈↓ ↓H␈↓1.  Add ␈↓↓isprod(e),␈↓ and ␈↓↓p1(e),␈↓ and ␈↓↓p1(e)␈↓ to the abstract syntax of the source language.

␈↓ ↓H␈↓2.  Add a term

␈↓ ↓H␈↓␈↓ ∧
␈↓↓␈↓αif␈↓↓ isprod(e) ␈↓αthen␈↓↓ value(p1(e),␈↓	x␈↓↓) ␈↓πx␈↓↓ value(p2(e),␈↓	x␈↓↓)␈↓ 

␈↓ ↓H␈↓to Equation (2.1).

␈↓ ↓H␈↓3.  Add
␈↓ ↓H␈↓␈↓ εH␈↓ 99


␈↓ ↓H␈↓␈↓ ∧T␈↓↓isprod(e) ∧ ␈↓	F␈↓↓(p1(e)) ∧ ␈↓	F␈↓↓(p2(e)) ⊃ ␈↓	F␈↓↓(e)␈↓ 

␈↓ ↓H␈↓to the hypotheses of the source language induction principle.

␈↓ ↓H␈↓4.␈α Add␈αan␈αinstruction␈α␈↓↓mul␈↓␈α␈↓↓x␈↓␈αand␈αthe␈αthree␈αsyntactical␈αfunctions␈α␈↓↓ismul(s),␈↓␈α␈↓↓adr(s),␈↓␈α␈↓↓mkmul(x)␈↓␈αto␈αthe
␈↓ ↓H␈↓abstract syntax of the object language together with the necessary relations among them.

␈↓ ↓H␈↓5.  Add to the definition (3.11) of ␈↓↓step␈↓ a term

␈↓ ↓H␈↓␈↓ β{␈↓↓␈↓αelse␈↓↓ ␈↓αif␈↓↓ ismul(s) ␈↓αthen␈↓↓ a(ac,c(adr(s),␈↓	h␈↓↓) ␈↓πx ␈↓↓c(ac,␈↓	h␈↓↓),␈↓	h␈↓↓). ␈↓ 

␈↓ ↓H␈↓6.  Add to the compiler a term

␈↓ ↓H␈↓␈↓ αH␈↓↓␈↓αif␈↓↓ isprod(e) ␈↓αthen␈↓↓ compile(p1(e),t) * mksto(t)
␈↓ ↓H␈↓↓␈↓ ∧λ* compile(p2(e),t + 1) * mkmul(t).

␈↓ ↓H␈↓7.  Add to the proof a case ␈↓↓isprod(e)␈↓ which parallels the case ␈↓↓issum(e)␈↓ exactly.

␈↓ ↓H␈↓The following other extensions are contemplated.
␈↓ ↓H␈↓␈↓ αH1.  Variable length sums.
␈↓ ↓H␈↓␈↓ αH2.  Sequences of assignment statements.
␈↓ ↓H␈↓␈↓ αH3.  Conditional expressions.
␈↓ ↓H␈↓␈↓ αH4.  ␈↓αgo to␈↓ statements in the source language.

␈↓ ↓H␈↓In␈α∞order␈α∞to␈α∞make␈α∞these␈α∞extensions␈α∞a␈α∞complete␈α∞revision␈α∞of␈α∞the␈α∞formalism␈α∞will␈α∞be␈α∞required.␈α
 1977
␈↓ ↓H␈↓note: These and more extensions were made in Painter's thesis [5].


␈↓ ↓H␈↓␈↓ ¬␈␈↓αReferences␈↓

␈↓ ↓H␈↓␈↓ αλ1.␈α
 J.␈αMcCarthy,␈α
␈↓↓Computer␈αprograms␈α
for␈αchecking␈α
mathematical␈αproofs,␈α
␈↓␈αProc.␈α
Sympos.␈αPure
␈↓ ↓H␈↓Math. Vol. 5, Amer. Math. Soc., Providence, R. I., 1962, pp. 219-227.

␈↓ ↓H␈↓␈↓ αλ2.␈α→ -----------,␈α→"A␈α~basis␈α→for␈α→a␈α→mathematical␈α~theory␈α→of␈α→computation"␈α~in␈α→␈↓↓Computer
␈↓ ↓H␈↓↓programming␈α∩and␈α⊃formal␈α∩systems,␈α∩␈↓edited␈α⊃by␈α∩P.␈α∩Braffort␈α⊃and␈α∩D.␈α∩ Hershberg,␈α⊃North-Holland,
␈↓ ↓H␈↓Amsterdam, 1963.

␈↓ ↓H␈↓␈↓ αλ3.␈α∂ -----------,␈α∂␈↓↓Towards␈α∂a␈α∂mathematical␈α∂theory␈α∂of␈α∂computation,␈α∂␈↓Proc.␈α∂ Internat.␈α∂Congr.␈α∞on
␈↓ ↓H␈↓Information Processing, 1962.

␈↓ ↓H␈↓␈↓ αλ4.␈α -----------,␈α␈↓↓A␈αformal␈αdescription␈αof␈αa␈αsubset␈αof␈αAlgol,␈α␈↓Proc.␈αConf.␈α on␈αFormal␈αLanguage
␈↓ ↓H␈↓Description Languages, Vienna, 1964.

␈↓ ↓H␈↓␈↓ αλ5.␈α∂J.␈α⊂Painter,␈α∂␈↓↓Semantic␈α∂correctness␈α⊂of␈α∂a␈α⊂compiler␈α∂for␈α∂an␈α⊂Algol-like␈α∂language,␈α⊂␈↓Ph.D.␈α∂thesis,
␈↓ ↓H␈↓Stanford University, Stanford, California, 1967.